$\forall$$i$,$x$:Id, $T$:Type, ${\it ks}$:(Knd List), $A$:es\_realizer\{i:l\}.
\\[0ex]($\neg$($\uparrow$R{-}occurs($A$; $i$; $x$))) $\Rightarrow$ R{-}compat\{i:l\}(Rframe($i$; $T$; $x$; ${\it ks}$); $A$)